Termination of the following Term Rewriting System could be proven:

Context-sensitive rewrite system:
The TRS R consists of the following rules:

f(a, X, X) → f(X, b, b)
b → a

The replacement map contains the following entries:

f: {2}
a: empty set
b: empty set


↳ CSR
  ↳ CSDependencyPairsProof
  ↳ Incomplete Giesl Middeldorp-Transformation

Context-sensitive rewrite system:
The TRS R consists of the following rules:

f(a, X, X) → f(X, b, b)
b → a

The replacement map contains the following entries:

f: {2}
a: empty set
b: empty set

Using Improved CS-DPs we result in the following initial Q-CSDP problem.

↳ CSR
  ↳ CSDependencyPairsProof
    ↳ QCSDP
      ↳ QCSDependencyGraphProof
  ↳ Incomplete Giesl Middeldorp-Transformation

Q-restricted context-sensitive dependency pair problem:
For all symbols f in {f, F} we have µ(f) = {2}.
The symbols in {U} are not replacing on any position.

The ordinary context-sensitive dependency pairs DPo are:

F(a, X, X) → F(X, b, b)
F(a, X, X) → B


The hidden terms of R are:

b

Every hiding context is built from:none

Hence, the new unhiding pairs DPu are :

U(b) → B

The TRS R consists of the following rules:

f(a, X, X) → f(X, b, b)
b → a

Q is empty.

The approximation of the Context-Sensitive Dependency Graph contains 1 SCC with 1 less node.


↳ CSR
  ↳ CSDependencyPairsProof
    ↳ QCSDP
      ↳ QCSDependencyGraphProof
        ↳ QCSDP
          ↳ QCSUsableRulesProof
  ↳ Incomplete Giesl Middeldorp-Transformation

Q-restricted context-sensitive dependency pair problem:
For all symbols f in {f, F} we have µ(f) = {2}.

The TRS P consists of the following rules:

F(a, X, X) → F(X, b, b)

The TRS R consists of the following rules:

f(a, X, X) → f(X, b, b)
b → a

Q is empty.

The following rules are not useable and can be deleted:

f(a, x0, x0) → f(x0, b, b)


↳ CSR
  ↳ CSDependencyPairsProof
    ↳ QCSDP
      ↳ QCSDependencyGraphProof
        ↳ QCSDP
          ↳ QCSUsableRulesProof
            ↳ QCSDP
              ↳ ConvertedToQDPProblemProof
  ↳ Incomplete Giesl Middeldorp-Transformation

Q-restricted context-sensitive dependency pair problem:
For all symbols f in {F} we have µ(f) = {2}.

The TRS P consists of the following rules:

F(a, X, X) → F(X, b, b)

The TRS R consists of the following rules:

b → a

Q is empty.

Converted QDP Problem, but could not keep Q or minimality.

↳ CSR
  ↳ CSDependencyPairsProof
    ↳ QCSDP
      ↳ QCSDependencyGraphProof
        ↳ QCSDP
          ↳ QCSUsableRulesProof
            ↳ QCSDP
              ↳ ConvertedToQDPProblemProof
                ↳ QDP
                  ↳ NonTerminationProof
  ↳ Incomplete Giesl Middeldorp-Transformation

Q DP problem:
The TRS P consists of the following rules:

F(a, X, X) → F(X, b, b)

The TRS R consists of the following rules:

b → a

Q is empty.
We have to consider all (P,Q,R)-chains.
We used the non-termination processor [17] to show that the DP problem is infinite.
Found a loop by narrowing to the right:

The TRS P consists of the following rules:

F(a, X, X) → F(X, b, b)

The TRS R consists of the following rules:

b → a


s = F(a, X, X) evaluates to t =F(X, a, a)

Thus s starts an infinite chain as s semiunifies with t with the following substitutions:



Rewriting sequence

F(a, a, a) → F(a, b, b)
with rule F(a, X, X) → F(X, b, b) and matcher [X / a].

F(a, b, b) → F(a, a, b)
with rule b → a at position [1] and matcher [ ]

F(a, a, b) → F(a, a, a)
with rule b → a at position [2] and matcher [ ]

Now applying the matcher to the start term leads to a term which is equal to the last term in the rewriting sequence


All these steps are and every following step will be a correct step w.r.t to Q.




We applied the Incomplete Giesl Middeldorp transformation [11] to transform the context-sensitive TRS to a usual TRS.

↳ CSR
  ↳ CSDependencyPairsProof
  ↳ Incomplete Giesl Middeldorp-Transformation
    ↳ QTRS
      ↳ RRRPoloQTRSProof

Q restricted rewrite system:
The TRS R consists of the following rules:

mark(f(x1, x2, x3)) → fActive(x1, mark(x2), x3)
fActive(x1, x2, x3) → f(x1, x2, x3)
mark(b) → bActive
bActive → b
mark(a) → a
fActive(a, X, X) → fActive(X, bActive, b)
bActive → a

Q is empty.

The following Q TRS is given: Q restricted rewrite system:
The TRS R consists of the following rules:

mark(f(x1, x2, x3)) → fActive(x1, mark(x2), x3)
fActive(x1, x2, x3) → f(x1, x2, x3)
mark(b) → bActive
bActive → b
mark(a) → a
fActive(a, X, X) → fActive(X, bActive, b)
bActive → a

Q is empty.
The following rules can be removed by the rule removal processor [15] because they are oriented strictly by a polynomial ordering:

fActive(x1, x2, x3) → f(x1, x2, x3)
bActive → b
mark(a) → a
bActive → a
Used ordering:
Polynomial interpretation [25]:

POL(a) = 1   
POL(b) = 0   
POL(bActive) = 2   
POL(f(x1, x2, x3)) = 1 + 2·x1 + x2 + 2·x3   
POL(fActive(x1, x2, x3)) = 2 + 2·x1 + x2 + 2·x3   
POL(mark(x1)) = 2 + 2·x1   




↳ CSR
  ↳ CSDependencyPairsProof
  ↳ Incomplete Giesl Middeldorp-Transformation
    ↳ QTRS
      ↳ RRRPoloQTRSProof
        ↳ QTRS
          ↳ RRRPoloQTRSProof

Q restricted rewrite system:
The TRS R consists of the following rules:

mark(f(x1, x2, x3)) → fActive(x1, mark(x2), x3)
mark(b) → bActive
fActive(a, X, X) → fActive(X, bActive, b)

Q is empty.

The following Q TRS is given: Q restricted rewrite system:
The TRS R consists of the following rules:

mark(f(x1, x2, x3)) → fActive(x1, mark(x2), x3)
mark(b) → bActive
fActive(a, X, X) → fActive(X, bActive, b)

Q is empty.
The following rules can be removed by the rule removal processor [15] because they are oriented strictly by a polynomial ordering:

mark(f(x1, x2, x3)) → fActive(x1, mark(x2), x3)
mark(b) → bActive
fActive(a, X, X) → fActive(X, bActive, b)
Used ordering:
Polynomial interpretation [25]:

POL(a) = 2   
POL(b) = 1   
POL(bActive) = 0   
POL(f(x1, x2, x3)) = 2 + 2·x1 + 2·x2 + 2·x3   
POL(fActive(x1, x2, x3)) = 2·x1 + x2 + x3   
POL(mark(x1)) = 2·x1   




↳ CSR
  ↳ CSDependencyPairsProof
  ↳ Incomplete Giesl Middeldorp-Transformation
    ↳ QTRS
      ↳ RRRPoloQTRSProof
        ↳ QTRS
          ↳ RRRPoloQTRSProof
            ↳ QTRS
              ↳ RisEmptyProof

Q restricted rewrite system:
R is empty.
Q is empty.

The TRS R is empty. Hence, termination is trivially proven.